@gares shall we merge?

We have to decide what to do with the code of eta and factory.sort, which is half commented

I would wait to talk about it live, maybe on Tuesday?

@CohenCyril this is green again. I could measure precisely the performances and:

• "factory sort" does not add anything per se
• "factory sort tac" has exactly the same performance

This Pr math-comp/math-comp#770 contains a cleanup commit and another one where I use HB.pack behind the scenes. To me, it looks like an improvement, especially since one does not need to retrofit some inheritance by sneaking a structure projection somewhere. After the last commit you can write HB.pack Key Tsomething Factory, which is quite natural, eg pose Kfield := FieldType K Kring KfieldMixin. (Kring is a structure, but HB.pack projects it to its class which is a factory, so you can use K as the real key, and after it all the stuff).

So to me it seems the factory sort via CS is superseded, since there is no performance loss.

The only mixed feeling left is that FooType becomes a notation (a grammar rule) and not a simple constant.
IMO, it is worth using, systematically, pose Kfield : fieldType := HB.pack K Kring KfieldMixin which requires no notation, works with planB and is only a few more chars per line. Then #[pack(short="xxx")] would enable the notation xxx, which is otherwise skipped. Finally, HB.pack would look less mysterious (it is clearly some HB code you can look up in the doc and not a magic constant with variable arity).

Once we merge this PR I can start playing with strategy again. Do you agree with the plan above (use HB.pack directly).

Yes, I agree.
How does HB.pack work with plan B BTW?

HB.pack is an exported tactic. Elpi Export tac is the same thing of tac-in-terms, it adds a grammar rule. But this time the grammar rule is just one and mentions HB, so it is more legit that it is global (it is governed by Import structures, not by Import GRing.Foo).

Being a grammar rule it receives the right loc, so in planB you get it replaced by Foo.Pack T (Foo.Class T M1 .. MN)

HB.pack is an exported tactic. Elpi Export tac is the same thing of tac-in-terms, it adds a grammar rule. But this time the grammar rule is just one and mentions HB, so it is more legit that it is global (it is governed by Import structures, not by Import GRing.Foo).

Being a grammar rule it receives the right loc, so in planB you get it replaced by Foo.Pack T (Foo.Class T M1 .. MN)

OK, so this means planB stops usercode from packing inside code... While before they "just" could not add a new structure...
Isn't this too much of a limitation for plan B to make sense?

OK, so this means planB stops usercode from packing inside code... While before they "just" could not add a new structure...

Can you exaplian better? I don't follow.

Can you exaplian better? I don't follow.

Yes sorry. As I understand it the purpose of HB plan B is to reassure HB users developing a library such as mathcomp, that they do not have to depend on elpi, they can translate everything and ship the code without elpi. The cost is the unability to add new structures, but the rest is supposed to work just fine. Now, if building an instance in the middle of the proof requires HB, then it impacts users as well... One could argue that without HB.instance it's already difficult to use HB though... so in the end I don't know, let's say it's fine like you propose.